M:MsgA, x:Id. x declared in M  M.ds(x) = Top  Type 

latex

Definitions	Top, t  T, x:A. B(x), b, A, b, , Prop, False, P  Q, Id, x. t(x), a:A fp B(a), IdDeq, x  dom(f), P & Q, P  Q, Unit, f(x)?z, M.ds(x), x declared in M, MsgA
Lemmas	msga wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, Id wf, bool wf, bnot wf, not wf, assert wf, top wf